es:ES, k:Knd, l:IdLnk, tg:Id, B, T:Type, f:(state@source(l)BT).
only k(v):B sends [tg,f(s,v)] : T on l  Prop 

latex

Definitions	t  T, True, P & Q, A & B, {T}, P  Q, x:A. B(x), T, ES, Id, state@i, source(l), b, sender(e), val(e), (state when e), E, 1of(t), SQType(T), Knd, Prop, kind(e), IdLnk, x(s1,s2), valtype(e), rcv(l,tg), x:A. B(x), loc(e), only k(v):B sends [tg,f(s;v)] : T on l
Lemmas	IdLnk wf, es-loc wf, rcv wf, es-valtype wf, subtype rel self, es-kind wf, Knd wf, Knd sq, es-E wf, es-state-when wf, es-val wf, es-sender wf, lsrc wf, es-state wf, squash wf, true wf, Id wf, event system wf, es-kind-rcv